\begin{tabbing}
ecl{-}trans{-}reachable(${\it ds}$;${\it da}$;$v$;$L$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $T$,${\it ks}$,$i$,$g$,$h$,$a$,$e$ = $v$ in \+
\\[0ex]$\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]c$\wedge$ \=(($\parallel$${\it L'}$$\parallel$ $<$ $\parallel$$L$$\parallel$)\+
\\[0ex]\& \=$x$\+
\\[0ex]=
\\[0ex]list\_accum(\=$x$,$a$.\=let $k$,${\it zz}$ = $a$\+\+
\\[0ex]in
\\[0ex]let $s$,$v$ = ${\it zz}$
\\[0ex]in
\\[0ex]if deq{-}member(KindDeq;$k$;${\it ks}$) then $g$($k$,$s$,$v$,$x$) else $x$ fi ;
\-\\[0ex]$i$;
\\[0ex]${\it L'}$)
\-\\[0ex]$\in$ $T$))
\-\-\-\-
\end{tabbing}